COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	axiom value:
C00004 ENDMK
C⊗;
axiom value:
	∀e xi.(value(e,xi) =
		IF isconst e THEN val e
		ELSE IF isvar e then c(e,xi)
		ELSE value(s1 e,xi) + value(s2 e,xi))
;;

axiom induction:
	∀e.(isconst e ∨ isvar e ∨ p s1 e ∧ p s2 e ⊃ p e) ⊃ ∀e.(p e)
;;

axiom compiler:
	∀e t u.(compile(e,t,u) =
		IF isconst e THEN mkli val e dt u
		ELSE IF isvar e THEN mkload map e
		ELSE compile(s1 e,t,mksto t dt compile(s2 t,t+1,mkadd t dt u)))
;;

axiom outcome:
	∀ prog eta.(outcome(prog,eta) =
		IF null prog THEN eta
		ELSE outcome(d prog,step(a prog,eta)))
;;

axiom step:
	∀s eta.(step(s,eta) =
		IF isli s THEN a(ac,arg s,eta)
		ELSE IF isload s THEN a(ac,c(adr s,eta),eta)
		ELSE IF issto s THEN a(adr s,c(ac,eta),eta)
		ELSE a(ac,c(ac,eta) + c(adr s,eta),eta))
;;